00100	PROBLEMS IN MATHEMATICAL THEORY OF COMPUTATION
00200	
00300		1. State and prove the parametrization of the solutions of
00400	x↑2 + y↑2 = z↑2 in 1st order logic or LCF.
00500	
00600		2. McCarthy airline reservation system.
00700	
00800		3. Prove correctness of functions transforming conditional
00900	expressions to canonical form in LCF or PC.
01000	
01100		4. Fermat's last theorem for n=4.  With much more machinery,
01200	Fermat's last theorem for n=3. See Hardy and Wright.